$\mathbb{N}$ $\in$ Type